FDL - Nuprl Lemma : fifo

Nuprl Lemma : fifo_wf

11,40

es:ES, C, T:Type, S:(C

), R:(C

), code:(j,i:C

e:{x:E| S(j,i,x)}

state@loc(e)

T),

decode:(i:C

e:{x:E| R(i,x)}

state@loc(e)

T).
for clients C sends FIFO from j to i via (S[j,i],code) receives at i via (R[i],decode)

Definitions x:A. B(x), , t T, for clients C sends FIFO from j to i via (S[j,i],codes) receives at i via (R[i],decodes), x:A. B(x), P & Q, P Q, A c B

Lemmas es-causle wf, es-E wf, es-state wf, es-loc wf, event system wf

Definitions	x:A. B(x), , t T, for clients C sends FIFO from j to i via (S[j,i],codes) receives at i via (R[i],decodes), x:A. B(x), P & Q, P Q, A c B
Lemmas	es-causle wf, es-E wf, es-state wf, es-loc wf, event system wf